#include <iostream>
#include <sstream>
#include <string>
#include <vector>
#include <set>
#include <string.h>
using namespace std;
#include "werePrincessInterface.h"

extern string Prop_to_String(Prop*);

void ReadLogicType(LogicType l
    , std::string &problem){
    if(l == And){ problem = problem + "&"; }
    else if(l == Or){ problem = problem + "|"; }
    else if(l == Imp){ problem = problem + "->"; }
    else{ }
}
void ReadOPType(OPType l
    , std::string &problem){
    if(l == Plus){ problem = problem + "+"; }
    else if(l == Minus){ problem = problem + "-"; }
    else if(l == Multi){ problem = problem + "*"; }
    else if(l == Divide){ problem = problem + "/"; }
    else{ }
}
void ReadPropType(PropType l
    , std::string &problem){
    if(l == LT){ problem = problem + "<"; }
    else if(l == GT){ problem = problem + ">"; }
    else if(l == Eq){ problem = problem + "="; }
    else{ }
}
void ReadQuantType(QuantType q
    , std::string &problem){
    if(q == Forall){ problem = problem + "forall"; }
    else if(q == Exist){ problem = problem + "exist"; }
    else{ }
}
void RecursiveReadExpr(Expr* e, std::vector<Expr*> &store_declaration
    , std::string &func
    , std::string &problem
    , std::set<Expr*> &quant_use){
    int i1, i2, flag;
    i1 = 0; i2 = 0; flag = 0;
    std::vector<Expr*>::iterator ve_it;
    if(typeid(*e) == typeid(IntExpr)){
        //std::cout << "IntExpr test" << std::endl;
        problem = problem + i2string(((IntExpr*)e)->i);
    }
    else if(typeid(*e) == typeid(VarExpr)){
        //std::cout << "VarExpr test " << store_declaration.size() << std::endl;
        for(i1 = 0; i1 < (int)store_declaration.size(); i1++){
            if(strcmp(((VarExpr*)store_declaration[i1])->x, ((VarExpr*)e)->x) == 0){
                flag = 1;
                break;
            }
            else{
            }
        }
        if(flag == 0){ 
            store_declaration.push_back(e); 
            quant_use.insert(e);
        }
        problem = problem + ((VarExpr*)e)->x;
    }
    else if(typeid(*e) == typeid(SelectExpr)){
        for(i1 = 0; i1 < (int)store_declaration.size(); i1++){
            //if(((SelectExpr*)e)->a == ((SelectExpr*)store_declaration[i1])){
            if(((SelectExpr*)e)->IsTheSameArray(*((SelectExpr*)store_declaration[i1]))){
                //cout << ((VarExpr*)(((SelectExpr*)e)->a))->x << endl;
                flag = 1;
                break;
            }
            else{
                //if(typeid(*(store_declaration[i1])) == typeid(SelectExpr)){
                //    cout << ((VarExpr*)(((SelectExpr*)(store_declaration[i1]))->a))->x  << endl;
                //}
            }
        }
        if(flag == 0){ 
            //store_declaration.push_back(e); 
            //quant_use.insert(e);
        }
        problem = problem + "select(";
        RecursiveReadExpr(((SelectExpr*)e)->a, store_declaration, func, problem, quant_use);
        problem = problem + ",";
        RecursiveReadExpr(((SelectExpr*)e)->i, store_declaration, func, problem, quant_use);
        problem = problem + ")";
    }
    else if(typeid(*e) == typeid(StoreExpr)){
        problem = problem + "store( ";
        RecursiveReadExpr(((StoreExpr*)e)->a, store_declaration, func, problem, quant_use);
        problem = problem + ", ";
        RecursiveReadExpr(((StoreExpr*)e)->i, store_declaration, func, problem, quant_use);
        problem = problem + ", ";
        RecursiveReadExpr(((StoreExpr*)e)->e, store_declaration, func, problem, quant_use);
        problem = problem + ")";
    }
    else if(typeid(*e) == typeid(BinExpr)){
        RecursiveReadExpr(((BinExpr*)e)->e1, store_declaration, func, problem, quant_use);
        ReadOPType(((BinExpr*)e)->op, problem);
        RecursiveReadExpr(((BinExpr*)e)->e2, store_declaration, func, problem, quant_use);
    }
    else{
    }
    return;
}
string RecursiveReadSelectExpra4(Expr* a){
    string result;
    if(typeid(*a) == typeid(SelectExpr)){
        result = RecursiveReadSelectExpra4(((SelectExpr*)a)->a);
    }
    else if(typeid(*a) == typeid(VarExpr)){
        result = ((VarExpr*)a)->x;
    }
    return result;
}
void RecursiveReadProp(Prop* p, std::vector<Expr*> &store_declaration
    , std::string &func
    , std::string &problem
    , std::set<Expr*> &quant_use){
    if(typeid(*p) == typeid(BoolProp)){
        if(((BoolProp*)p)->b == true){
            problem = problem + "true";
        }
        else{
            problem = problem + "false";
        }
    }
    else if(typeid(*p) == typeid(NegProp)){
        problem = problem + "!(";
        RecursiveReadProp(((NegProp*)p)->p, store_declaration, func, problem, quant_use);
        problem = problem + ")";
    }
    else if(typeid(*p) == typeid(BinProp)){
        RecursiveReadProp(((BinProp*)p)->p1, store_declaration, func, problem, quant_use);
        ReadLogicType(((BinProp*)p)->l, problem);
        RecursiveReadProp(((BinProp*)p)->p2, store_declaration, func, problem, quant_use);
    }
    else if(typeid(*p) == typeid(InequProp)){
        //std::cout << "InequProp test" << std::endl;
        RecursiveReadExpr(((InequProp*)p)->e1, store_declaration, func, problem, quant_use);
        ReadPropType(((InequProp*)p)->p, problem);
        RecursiveReadExpr(((InequProp*)p)->e2, store_declaration, func, problem, quant_use);
    }
    else if(typeid(*p) == typeid(QuantProp)){
        string before_quant;
        RecursiveReadProp(((QuantProp*)p)->p, store_declaration, func, problem, quant_use);
        if(((QuantProp*)p)->t == Forall){
            before_quant = before_quant + "\\forall int ";
        }
        else if(((QuantProp*)p)->t == Exist){
            before_quant = before_quant + "\\exist int ";
        }
        else{
        }
        int set_size;
        set<Expr*>::iterator set_it;
        set_size = 0;
        for(set_it = quant_use.begin(); set_it != quant_use.end(); set_it++){
            if(typeid(*set_it) == typeid(VarExpr)){
                before_quant = before_quant + ((VarExpr*)(*set_it))->x;
            }
            else if(typeid(*set_it) == typeid(SelectExpr)){
                before_quant = before_quant + RecursiveReadSelectExpra4(((SelectExpr*)(*set_it))->a);
            }
            else{
            }
            set_size = set_size + 1;
            if(set_size == (int)quant_use.size()){
                before_quant = before_quant + ";";
            }
            else{
                before_quant = before_quant + ", ";
            }
        }
        quant_use.clear();
        problem = before_quant + problem;
    }
    else{
    }
    return;
}
std::string CombineExpr2String(vector<Prop*> v_p){
    int i1, i2;
    std::vector<Expr*> store_declaration;
    std::string func, problem, total;
    std::set<Expr*> quant_use;
    problem = problem + "\\problem {";
    for(i2 =0; i2 < (int)v_p.size(); i2++){
        problem = problem + "\\part[p";
        problem = problem + i2string(i2);
        problem = problem + "] ";
        if(typeid(*(v_p[i2])) == typeid(BinProp) && i2 != (int)v_p.size()-1){
            problem = problem + "(";
        }
        if(i2 == (int)v_p.size()-1){
            problem = problem + "(";
        }
        RecursiveReadProp(v_p[i2], store_declaration, func, problem, quant_use);
        if(typeid(*(v_p[i2])) == typeid(BinProp) && i2 != (int)v_p.size()-1){
            problem = problem + ")";
        }
        if(i2 != (int)v_p.size()-1){
            problem = problem + " & ";
        }
        else{
            problem = problem + " )-> false";
        }
    }
    //std::cout << "store_declaration size = " << store_declaration.size() << std::endl;
    problem = problem + "}\n";
    func = func + "\\functions {int ";
    for(i1 = 0; i1 < (int)store_declaration.size(); i1++){
        if(typeid(*(store_declaration[i1])) == typeid(VarExpr)){
            func = func + ((VarExpr*)(store_declaration[i1]))->x;
        }
        else{
            func = func + RecursiveReadSelectExpra4(((SelectExpr*)(store_declaration[i1]))->a);
        }
        if(i1 == (int)store_declaration.size()-1){
            func = func + ";";
        }
        else{
            func = func + ",";
        }
    }
    func = func + "}";
    total = func + "";
    total = total + problem;
    //std::cout << problem << std::endl;
    //std::cout << func << std::endl;
    return total;
}
//test nornal Inequ Prop------------------------------------OK
void test0(piped_processt &p, vector<Prop*> &v_p1){
//void test0(){
    Expr *ei1, *ei2, *a;
    ei1 = new IntExpr;
    ((IntExpr*)ei1)->i = 1;
    ei2 = new IntExpr;
    ((IntExpr*)ei2)->i = 2;
    a = new VarExpr;
    strcpy(((VarExpr*)a)->x, "a");
    Prop *p1, *p2;
    vector<Prop*> v_p;
    p1 = new InequProp;
    ((InequProp*)p1)->e1 = a;
    ((InequProp*)p1)->p = Eq;
    ((InequProp*)p1)->e2 = ei1;
    //p1 : a == 1
    p2 = new InequProp;
    ((InequProp*)p2)->e1 = a;
    ((InequProp*)p2)->p = Eq;
    ((InequProp*)p2)->e2 = ei2;
    //p2 : a == 2
    v_p.push_back(p1);
    v_p.push_back(p2);
    std::string str;
    str = CombineExpr2String(v_p);
    std::cout << str << std::endl;
    p.write(str);
    p.write("interpolate.\n");   // no \interpolant clauses are required

    str = p.read_line();
    while (str != ".") {  // wait for the end of the response
      cout << str << endl;
      PrincessFormulaParser pfp(str);
      v_p1.push_back(pfp.parse());
      str = p.read_line();
    }

}
//test array Expr -------------------------------------------OK
void test1(piped_processt &p, vector<Prop*> &v_p1){
//void test1(){
    std::string str;
    Expr *ei1, *ei2, *a, *b, *M1, *M2;
    ei1 = new IntExpr;
    ((IntExpr*)ei1)->i = 1;
    ei2 = new IntExpr;
    ((IntExpr*)ei2)->i = 2;
    a = new VarExpr;
    strcpy(((VarExpr*)a)->x, "a");
    b = new VarExpr;
    strcpy(((VarExpr*)b)->x, "b");
    M1 = new SelectExpr;
    ((SelectExpr*)M1)->a = new VarExpr;
    strcpy(((VarExpr*)(((SelectExpr*)M1)->a))->x, "M1");
    ((SelectExpr*)M1)->i = a;
    M2 = new SelectExpr;
    ((SelectExpr*)M2)->a = new VarExpr;
    strcpy(((VarExpr*)(((SelectExpr*)M2)->a))->x, "M2");
    ((SelectExpr*)M2)->i = a;
    Prop *p1, *p2, *p3, *p4, *p5;
    vector<Prop*> v_p;
    // p1 : a = 1;
    p1 = new InequProp;
    ((InequProp*)p1)->e1 = a;
    ((InequProp*)p1)->p = Eq;
    ((InequProp*)p1)->e2 = ei1;
    // p2 : b = 2;
    p2 = new InequProp;
    ((InequProp*)p2)->e1 = b;
    ((InequProp*)p2)->p = Eq;
    ((InequProp*)p2)->e2 = ei2;
    // p3 : M1[a] = 1
    p3 = new InequProp;
    ((InequProp*)p3)->e1 = M1;
    ((InequProp*)p3)->p = Eq;
    ((InequProp*)p3)->e2 = ei1;
     // p4 : M2[a] = 2
    p4 = new InequProp;
    ((InequProp*)p4)->e1 = M2;
    ((InequProp*)p4)->p = Eq;
    ((InequProp*)p4)->e2 = ei2;
    // p : M2[a] = 1
    p5 = new InequProp;
    ((InequProp*)p5)->e1 = M2;
    ((InequProp*)p5)->p = Eq;
    ((InequProp*)p5)->e2 = M1;
    //push to v_p
    v_p.push_back(p1);
    v_p.push_back(p2);
    v_p.push_back(p3);
    v_p.push_back(p4);
    v_p.push_back(p5);
    //change to input string
    str = CombineExpr2String(v_p);
    std::cout << str << std::endl;
   
    //p.write("\\functions {int M, M', a, x, b, c;}\\problem {(\\part[p0] M' = store(M, a, x) & \\part[p1] (b != c & select(M',b) != select(M,b) & select(M',c) != select(M,c)) )-> false}\n");
    p.write(str);
    p.write("interpolate.\n");   // no \interpolant clauses are required
    str = p.read_line();
    while (str != ".") {  // wait for the end of the response
      cout << str << endl;
      PrincessFormulaParser pfp(str);
      v_p1.push_back(pfp.parse());
      str = p.read_line();
    }
}
// test 2 d9mention array
void test2(piped_processt &p, vector<Prop*> &v_p1){
    //a[b[i]] = b[ 10-i] /\ i =(10+j) /\ b[j]=a[j +5]
    Expr *a1, *a2, *b1, *b2, *b3, *i, *j, *e5, *e10, *com1, *com2, *com3;
    Prop *p1, *p2, *p3;
    vector<Prop*> v_p;
    i = new VarExpr;
    strcpy(((VarExpr*)i)->x, "i");
    j = new VarExpr;
    strcpy(((VarExpr*)j)->x, "j");
    e5 = new IntExpr;
    ((IntExpr*)e5)->i = 5;
    e10 = new IntExpr;
    ((IntExpr*)e10)->i = 10;
    com1 = new BinExpr;
    ((BinExpr*)com1)->e1 = e10;
    ((BinExpr*)com1)->op = Minus;
    ((BinExpr*)com1)->e2 = i;
    com2 = new BinExpr;
    ((BinExpr*)com2)->e1 = e10;
    ((BinExpr*)com2)->op = Plus;
    ((BinExpr*)com2)->e2 = j;
    b1 = new SelectExpr;
    ((SelectExpr*)b1)->a = new VarExpr;
    strcpy(((VarExpr*)(((SelectExpr*)b1)->a))->x, "b");
    ((SelectExpr*)b1)->i = i;
    a1 = new SelectExpr;
    ((SelectExpr*)a1)->a = new VarExpr;
    strcpy(((VarExpr*)(((SelectExpr*)a1)->a))->x, "a");
    ((SelectExpr*)a1)->i = b1;
    b2 = new SelectExpr;
    ((SelectExpr*)b2)->a = new VarExpr;
    strcpy(((VarExpr*)(((SelectExpr*)b2)->a))->x, "b");
    ((SelectExpr*)b2)->i = com1;
    b3 = new SelectExpr;
    ((SelectExpr*)b3)->a = new VarExpr;
    strcpy(((VarExpr*)(((SelectExpr*)b3)->a))->x, "b");
    ((SelectExpr*)b3)->i = j;
    com3 = new BinExpr;
    ((BinExpr*)com3)->e1 = j;
    ((BinExpr*)com3)->op = Plus;
    ((BinExpr*)com3)->e2 = e5;
    a2 = new SelectExpr;
    ((SelectExpr*)a2)->a = new VarExpr;
    strcpy(((VarExpr*)(((SelectExpr*)a2)->a))->x, "a");
    ((SelectExpr*)a2)->i = com3;
    p1 = new InequProp;
    ((InequProp*)p1)->e1 = a1;
    ((InequProp*)p1)->p = Eq;
    ((InequProp*)p1)->e2 = b2;
    p2 = new InequProp;
    ((InequProp*)p2)->e1 = i;
    ((InequProp*)p2)->p = Eq;
    ((InequProp*)p2)->e2 = com2;
    p3 = new InequProp;
    ((InequProp*)p3)->e1 = b3;
    ((InequProp*)p3)->p = Eq;
    ((InequProp*)p3)->e2 = a2;
    /*comp1 = new BinProp;
    ((BinProp*)comp1)->p1 = p1;
    ((BinProp*)comp1)->l = And;
    ((BinProp*)comp1)->p2 = p2;
    comp2 = new BinProp;
    ((BinProp*)comp2)->p1 = comp1;
    ((BinProp*)comp2)->l = And;
    ((BinProp*)comp2)->p2 = p3;*/
    v_p.push_back(p1);
    v_p.push_back(p2);
    v_p.push_back(p3);

    std::string str;
    str = CombineExpr2String(v_p);
    cout << str << endl;
    //str = "\\functions { int a, b, i, j; } \\problem { select(a,select(b, i)) = select(b, 10-i) & i = 10+j & select(b, j) = select(a, j+5) -> false } \n";
    p.write(str);
    p.write("interpolate.\n");   // no \interpolant clauses are required
    str = p.read_line();
    while (str != ".") {  // wait for the end of the response
      cout << str << endl;
      PrincessFormulaParser pfp(str);
      v_p1.push_back(pfp.parse());
      str = p.read_line();
    }
}
void test3(piped_processt &p){
    //test a[i][j] = 1 /\ a[i][j] = 2
    string str;
    str = "\\functions {int x1,x1_xt;}\\problem {\\part[p0] (true&!(x1_xt<3)) & \\part[p1] (true&x1=x1_xt+1 )-> false}\n";
    //str = "\\functions {int x1,x1_1;}\\problem {\\part[p0] (true&!(x1+1<3)&true&x1+1=x1_1+1) & \\part[p1] (true&x1<2 )-> false}\n";
    vector<Prop*> v_p;
    p.write(str);
    p.write("interpolate.\n");   // no \interpolant clauses are required
    str = p.read_line();
    while (str != ".") {  // wait for the end of the response
      cout << str << endl;
      if(str.compare("VALID") != 0 && str.compare("INVALID") != 0 && str.compare("true") != 0 && str.compare("false") != 0){
          PrincessFormulaParser pfp(str);
          v_p.push_back(pfp.parse());
          cout << "Prop : " << Prop_to_String(v_p[0]) << endl;
      }
      str = p.read_line();
    }
}
void test4(piped_processt &p){

    string str;
    str = "\\functions {  int x, y, z;  int ar;}\\problem {  \\part[p0] (select(ar, x) = 1)->  \\part[p1] (select(ar, y) >= select(ar, x))->  \\part[p2] (z = select(ar, y)+1)->  \\part[p3] (z < 0)->  false }\n";
    p.write(str);
    p.write("interpolate.\n");   // no \interpolant clauses are required
    str = p.read_line();
    while (str != ".") {  // wait for the end of the response
      cout << str << endl;
      str = p.read_line();
    }
}
void test5(piped_processt &p){
    string str = "\\functions {  int M, M', a, x, b, c;}\\problem {  \\part[p0] M' = store(M, a, x) &  \\part[p1] (b != c & select(M',b) != select(M,b) & select(M',c) != select(M,c))  ->  false}\n";
    p.write(str);
    p.write("interpolate.\n");   // no \interpolant clauses are required
    str = p.read_line();
    while (str != ".") {  // wait for the end of the response
      cout << str << endl;
      str = p.read_line();
    }

}
void test6(piped_processt &p){
    string str = "\\functions {  int f(int);  int g(int, int);  int h(int);  int a, b;}\n \\predicates {  p(int, int); }\n\\problem {  \\forall int x1, x2; (g(x1,x2)=0 | h(x2)=0)->  \\forall int x1; g(f(x1), b)+1 <= f(x1)->  h(b) = 1->  f(a) = 0->  false}\n";
    p.write(str);
    p.write("interpolate.\n");   // no \interpolant clauses are required
    str = p.read_line();
    while (str != ".") {  // wait for the end of the response
      cout << str << endl;
      str = p.read_line();
    }
   
}//cav_ex2.pri fail
void test7(piped_processt &p){
    string str = "\\problem {  \\forall int a, b; (a = b -> eqArrays(a, b) = 0)&  \\forall int a, b, x; (eqArrays(a, b)=0 -> select(a, x) = select(b, x))&  \\forall int a; (eqArrays(a, a)=0)&  \\forall int a, b, c; (eqArrays(a, b)=0 -> eqArrays(b, c)=0 -> eqArrays(a, c)=0)&  \\forall int a, b; (eqArrays(a, b)=0 -> eqArrays(b, a)=0)&  \\forall int a, b, x, i; (eqArrays(a, b)=0 -> eqArrays(store(a, x, i), store(b, x, i))=0)&  \\forall int a, b, x, i, j;     (eqArrays(store(a, x, i), store(b, x, j))=0 -> i = j)}\n";
    p.write(str);
    p.write("interpolate.\n");   // no \interpolant clauses are required
    str = p.read_line();
    while (str != ".") {  // wait for the end of the response
      cout << str << endl;
      str = p.read_line();
    }

}
void wolverInterface0(piped_processt &p, vector<Prop*> &v_p1){
    Expr *x, *y, *z, *e5, *e1, *em1, *e0, *em5, *e2, *em2, *e13, *em13, *e20, *comxy, *comy13;
    x = new VarExpr;
    y = new VarExpr;
    z = new VarExpr;
    strcpy(((VarExpr*)x)->x, "x");
    strcpy(((VarExpr*)y)->x, "y");
    strcpy(((VarExpr*)z)->x, "z");
    e0 = new IntExpr;
    e1 = new IntExpr;
    em1 = new IntExpr;
    e2 = new IntExpr;
    em2 = new IntExpr;
    e5 = new IntExpr;
    em5 = new IntExpr;
    e13 = new IntExpr;
    em13 = new IntExpr;
    e20 = new IntExpr;
    ((IntExpr*)e0)->i = 0;
    ((IntExpr*)e1)->i = 1;
    ((IntExpr*)em1)->i = -1;
    ((IntExpr*)e2)->i = 2;
    ((IntExpr*)em2)->i = -1;
    ((IntExpr*)e5)->i = 5;
    ((IntExpr*)em5)->i = -5;
    ((IntExpr*)e13)->i = 13;
    ((IntExpr*)em13)->i = -13;
    ((IntExpr*)e20)->i = 20;
    comxy = new BinExpr;
    ((BinExpr*)comxy)->e1 = x;
    ((BinExpr*)comxy)->op = Minus;
    ((BinExpr*)comxy)->e2 = y;
    comy13 = new BinExpr;
    ((BinExpr*)comy13)->e1 = y;
    ((BinExpr*)comy13)->op = Plus;
    ((BinExpr*)comy13)->e2 = e13;
    Prop *p1, *p2, *p3,*p1_1, *p1_2, *p4, *p5, *p2_1, *p6, *p7, *p8;
    vector<Prop*> v_p;
    p1 = new InequProp;
    ((InequProp*)p1)->e1 = x;
    ((InequProp*)p1)->e2 = em5;
    ((InequProp*)p1)->p = LT;
    p2 = new InequProp;
    ((InequProp*)p2)->e1 = x;
    ((InequProp*)p2)->e2 = e0;
    ((InequProp*)p2)->p = GT;
    p3 = new InequProp;
    ((InequProp*)p3)->e1 = x;
    ((InequProp*)p3)->e2 = e5;
    ((InequProp*)p3)->p = LT;
    p1_1 = new BinProp;
    ((BinProp*)p1_1)->p1 = p1;
    ((BinProp*)p1_1)->p2 = p2;
    ((BinProp*)p1_1)->l = Or;
    p1_2 = new BinProp;
    ((BinProp*)p1_2)->p1 = p1_1;
    ((BinProp*)p1_2)->p2 = p3;
    ((BinProp*)p1_2)->l = And;
    v_p.push_back(p1_2);
    p4 = new InequProp;
    ((InequProp*)p4)->e1 = comxy;
    ((InequProp*)p4)->e2 = e2;
    ((InequProp*)p4)->p = LT;
    p5 = new InequProp;
    ((InequProp*)p5)->e1 = comxy;
    ((InequProp*)p5)->e2 = em2;
    ((InequProp*)p5)->p = GT;
    p2_1 = new BinProp;
    ((BinProp*)p2_1)->p1 = p4;
    ((BinProp*)p2_1)->p2 = p5;
    ((BinProp*)p2_1)->l = And;
    v_p.push_back(p2_1);
    p6 = new InequProp;
    ((InequProp*)p6)->e1 = z;
    ((InequProp*)p6)->e2 = comy13;
    ((InequProp*)p6)->p = Eq;
    v_p.push_back(p6);
    p7 = new InequProp;
    ((InequProp*)p7)->e1 = z;
    ((InequProp*)p7)->e2 = e20;
    ((InequProp*)p7)->p = LT;
    p8 = new NegProp;
    ((NegProp*)p8)->p = p7;
    v_p.push_back(p8);     
    std::string str;
    str = CombineExpr2String(v_p);
    cout << str << endl;
    //str = "\\functions {  int x, y, z;}\n \\problem {  \\part[p0] (x <= -5 | x >= 0 & x <= 5)->  \\part[p1] (x-y <= 2 & x-y >= -2)->  \\part[p2] (z = y + 13)->  \\part[p3] (z > 20)->  false}\n";
    //str = "\\functions {  int x, y, z;}\n \\problem {  \\part[p0] x <= -5 | x >= 0 & x <= 5 &  \\part[p1] x-y <= 2 & x-y >= -2 &  \\part[p2] z = y + 13 &  \\part[p3] (z > 20)->  false}\n";
    //str = "\\functions {  int x, y, z;}\n \\problem {  \\part[p0] (x <= -5 | x >= 0 & x <= 5) &  \\part[p1] ( x-y <= 2 & x-y >= -2 )->  false}\n";
    cout << str << endl;
    p.write(str);
    p.write("interpolate.\n");   // no \interpolant clauses are required

}
void wolverInterface1(piped_processt &p, vector<Prop*> &v_p1){
    Expr *x, *y, *z, *e5, *e1, *em1, *e0, *em5, *e2, *em2, *e11, *e13, *em13, *e20, *comxy, *comy13, *com2x, *com2xy;
    x = new VarExpr;
    y = new VarExpr;
    z = new VarExpr;
    strcpy(((VarExpr*)x)->x, "x");
    strcpy(((VarExpr*)y)->x, "y");
    strcpy(((VarExpr*)z)->x, "z");
    e0 = new IntExpr;
    e1 = new IntExpr;
    em1 = new IntExpr;
    e2 = new IntExpr;
    em2 = new IntExpr;
    e5 = new IntExpr;
    em5 = new IntExpr;
    e11 = new IntExpr;
    e13 = new IntExpr;
    em13 = new IntExpr;
    e20 = new IntExpr;
    ((IntExpr*)e0)->i = 0;
    ((IntExpr*)e1)->i = 1;
    ((IntExpr*)em1)->i = -1;
    ((IntExpr*)e2)->i = 2;
    ((IntExpr*)em2)->i = -1;
    ((IntExpr*)e5)->i = 5;
    ((IntExpr*)em5)->i = -5;
    ((IntExpr*)e11)->i = 11;
    ((IntExpr*)e13)->i = 13;
    ((IntExpr*)em13)->i = -13;
    ((IntExpr*)e20)->i = 20;
    comxy = new BinExpr;
    ((BinExpr*)comxy)->e1 = x;
    ((BinExpr*)comxy)->op = Minus;
    ((BinExpr*)comxy)->e2 = y;
    comy13 = new BinExpr;
    ((BinExpr*)comy13)->e1 = y;
    ((BinExpr*)comy13)->op = Plus;
    ((BinExpr*)comy13)->e2 = e13;
    com2x = new BinExpr;
    ((BinExpr*)com2x)->e1 = e2;
    ((BinExpr*)com2x)->op = Multi;
    ((BinExpr*)com2x)->e2 = x;
    com2xy = new BinExpr;
    ((BinExpr*)com2xy)->e1 = com2x;
    ((BinExpr*)com2xy)->op = Minus;
    ((BinExpr*)com2xy)->e2 = y;
    Prop *p1, *p2, *p3,*p1_1, *p1_2, *p4, *p5, *p2_1, *p6, *p7;
    vector<Prop*> v_p;
    p1 = new InequProp;
    ((InequProp*)p1)->e1 = x;
    ((InequProp*)p1)->e2 = em5;
    ((InequProp*)p1)->p = LT;
    p2 = new InequProp;
    ((InequProp*)p2)->e1 = x;
    ((InequProp*)p2)->e2 = e0;
    ((InequProp*)p2)->p = GT;
    p3 = new InequProp;
    ((InequProp*)p3)->e1 = x;
    ((InequProp*)p3)->e2 = e5;
    ((InequProp*)p3)->p = LT;
    p1_1 = new BinProp;
    ((BinProp*)p1_1)->p1 = p1;
    ((BinProp*)p1_1)->p2 = p2;
    ((BinProp*)p1_1)->l = Or;
    p1_2 = new BinProp;
    ((BinProp*)p1_2)->p1 = p1_1;
    ((BinProp*)p1_2)->p2 = p3;
    ((BinProp*)p1_2)->l = And;
    v_p.push_back(p1_2);
    p4 = new InequProp;
    ((InequProp*)p4)->e1 = comxy;
    ((InequProp*)p4)->e2 = e1;
    ((InequProp*)p4)->p = LT;
    p5 = new InequProp;
    ((InequProp*)p5)->e1 = com2xy;
    ((InequProp*)p5)->e2 = em1;
    ((InequProp*)p5)->p = GT;
    p2_1 = new BinProp;
    ((BinProp*)p2_1)->p1 = p4;
    ((BinProp*)p2_1)->p2 = p5;
    ((BinProp*)p2_1)->l = And;
    v_p.push_back(p2_1);
    p6 = new InequProp;
    ((InequProp*)p6)->e1 = z;
    ((InequProp*)p6)->e2 = comy13;
    ((InequProp*)p6)->p = Eq;
    v_p.push_back(p6);
    p7 = new InequProp;
    ((InequProp*)p7)->e1 = z;
    ((InequProp*)p7)->e2 = e11;
    ((InequProp*)p7)->p = Eq;
    v_p.push_back(p7);
    std::string str;
    str = CombineExpr2String(v_p);
    cout << str << endl;
    p.write(str);
    p.write("interpolate.\n");   // no \interpolant clauses are required
    str = p.read_line();
    while (str != ".") {  // wait for the end of the response
      cout << str << endl;
      PrincessFormulaParser pfp(str);
      v_p1.push_back(pfp.parse());
      str = p.read_line();
    }
    cout << "v_p1.size = "  << v_p1.size() << endl;

}
void wolverInterface2(piped_processt &p, vector<Prop*> &v_p1){
    Expr *x, *ar, *select_arx, *select_ary, *y, *z, *e1, *e0, *comy1;
    x = new VarExpr;
    y = new VarExpr;
    z = new VarExpr;
    ar = new VarExpr;
    strcpy(((VarExpr*)x)->x, "x");
    strcpy(((VarExpr*)y)->x, "y");
    strcpy(((VarExpr*)z)->x, "z");
    strcpy(((VarExpr*)ar)->x, "ar");
    e1 = new IntExpr;
    e0 = new IntExpr;
    ((IntExpr*)e1)->i = 1;
    ((IntExpr*)e0)->i = 0;
    select_arx = new SelectExpr;
    select_ary = new SelectExpr;
    ((SelectExpr*)select_arx)->a = ar;
    ((SelectExpr*)select_arx)->i = x;
    ((SelectExpr*)select_ary)->a = ar;
    ((SelectExpr*)select_ary)->i = y;
    comy1 = new BinExpr;
    ((BinExpr*)comy1)->e1 = select_ary;
    ((BinExpr*)comy1)->e2 = e1;
    ((BinExpr*)comy1)->op = Plus;
    Prop *p1, *p2, *p3, *p4;
    vector<Prop*> v_p;
    p1 = new InequProp;
    ((InequProp*)p1)->e1 = select_arx;
    ((InequProp*)p1)->e2 = e1;
    ((InequProp*)p1)->p = Eq;
    v_p.push_back(p1);
    p2 = new InequProp;
    ((InequProp*)p2)->e1 = select_arx;
    ((InequProp*)p2)->e2 = select_ary;
    ((InequProp*)p2)->p = GT;
    v_p.push_back(p2);
    p3 = new InequProp;
    ((InequProp*)p3)->e1 = z;
    ((InequProp*)p3)->e2 = comy1;
    ((InequProp*)p3)->p = Eq;
    v_p.push_back(p3);
    p4 = new InequProp;
    ((InequProp*)p4)->e1 = z;
    ((InequProp*)p4)->e2 = e0;
    ((InequProp*)p4)->p = LT;
    v_p.push_back(p4);
    std::string str;
    str = CombineExpr2String(v_p);
    cout << str << endl;
    //str = "\\functions {  int x, y, z;  int ar;}\n\\problem {  \\part[p0] select(ar, x) = 1 &  \\part[p1] select(ar, y) >= select(ar, x) &  \\part[p2] z = select(ar, y)+1 &  \\part[p3] (z < 0)->  false}\n";
    //std:cout << str << std::endl;
    p.write(str);
    p.write("interpolate.\n");   // no \interpolant clauses are required
    str = p.read_line();
    while (str != ".") {  // wait for the end of the response
      cout << str << endl;
      PrincessFormulaParser pfp(str);
      v_p1.push_back(pfp.parse());
      str = p.read_line();
    }

}
void wolverInterface3(piped_processt &p, vector<Prop*> &v_p1){
    Expr *M, *Mp, *a, *b, *c, *x, *storeM, *selectMpb, *selectMb, *selectMpc, *selectMc;
    M = new VarExpr;
    Mp = new VarExpr;
    a = new VarExpr;
    b = new VarExpr;
    c = new VarExpr;
    x = new VarExpr;
    strcpy(((VarExpr*)a)->x, "a");
    strcpy(((VarExpr*)b)->x, "b");
    strcpy(((VarExpr*)c)->x, "c");
    strcpy(((VarExpr*)x)->x, "x");
    strcpy(((VarExpr*)M)->x, "M");
    strcpy(((VarExpr*)Mp)->x, "Mp");
    storeM = new StoreExpr;
    selectMpb = new SelectExpr;
    selectMb = new SelectExpr;
    selectMpc = new SelectExpr;
    selectMc = new SelectExpr;
    ((StoreExpr*)storeM)->a = M;
    ((StoreExpr*)storeM)->i = a;
    ((StoreExpr*)storeM)->e = x;
    ((SelectExpr*)selectMb)->a = M;
    ((SelectExpr*)selectMb)->i = b;
    ((SelectExpr*)selectMpb)->a = Mp;
    ((SelectExpr*)selectMpb)->i = b;
    ((SelectExpr*)selectMc)->a = M;
    ((SelectExpr*)selectMc)->i = c;
    ((SelectExpr*)selectMpc)->a = Mp;
    ((SelectExpr*)selectMpc)->i = c;
    Prop *p1, *p2, *p2n, *p3, *p3n, *p4, *p4n, *p5, *p6;
    vector<Prop*> v_p;
    p1 = new InequProp;
    ((InequProp*)p1)->e1 = Mp;
    ((InequProp*)p1)->e2 = storeM;
    ((InequProp*)p1)->p = Eq;
    v_p.push_back(p1);
    p2 = new InequProp;
    ((InequProp*)p2)->e1 = b;
    ((InequProp*)p2)->e2 = c;
    ((InequProp*)p2)->p = Eq;
    p2n = new NegProp;
    ((NegProp*)p2n)->p = p2;
    p3 = new InequProp;
    ((InequProp*)p3)->e1 = selectMpb;
    ((InequProp*)p3)->e2 = selectMb;
    ((InequProp*)p3)->p = Eq;
    p3n = new NegProp;
    ((NegProp*)p3n)->p = p3;
    p4 = new InequProp;
    ((InequProp*)p4)->e1 = selectMpc;
    ((InequProp*)p4)->e2 = selectMc;
    ((InequProp*)p4)->p = Eq;
    p4n = new NegProp;
    ((NegProp*)p4n)->p = p4;
    p5 = new BinProp;
    ((BinProp*)p5)->p1 = p2n;
    ((BinProp*)p5)->p2 = p3n;
    ((BinProp*)p5)->l = And;
    p6 = new BinProp;
    ((BinProp*)p6)->p1 = p5;
    ((BinProp*)p6)->p2 = p4n;
    ((BinProp*)p6)->l = And;
    v_p.push_back(p6);
    std::string str;
    str = CombineExpr2String(v_p);
    cout << str << endl;
    //str = "\\functions {  int M, M', a, x, b, c;}\\problem {  \\part[p0] M' = store(M, a, x) &  \\part[p1] (b != c & select(M',b) != select(M,b) & select(M',c) != select(M,c))  ->  false}\n";
    //str = "\\functions {int Mp,M,a,x,b,c;   }    \\problem { \\part[p0] Mp=store( M, a, x) & \\part[p1] (!(b=c)&!(select(Mp,b)=select(M,b))&!(select(Mp,c)=select(M,c)) )-> false}\n";
    //str = "\\functions {  int M, M', a, x, b, c;}\\problem {  \\part[p0] M' = store(M, a, x) &  \\part[p1] (b != c & select(M',b) != select(M,b) & select(M',c) != select(M,c))  ->  false}\n";
    cout << str << endl;
    p.write(str);
    p.write("interpolate.\n");   // no \interpolant clauses are required
    str = p.read_line();
    while (str != ".") {  // wait for the end of the response
      cout << str << endl;
      PrincessFormulaParser pfp(str);
      v_p1.push_back(pfp.parse());
      str = p.read_line();
    }
}
void werePrincessUnitTest(){
    string s = "./princess-2011-05-27/werePrincess";
    vector<string> vs; 
    piped_processt p(s, vs);
    test3(p);
}
/*int main(){
    string s = "/home/quake/princess-bin-2011-05-05/werePrincess";
    vector<string> vs; 
    piped_processt p(s, vs);
    vector<Prop*> v_p;
    //test0(p, v_p);
    //test1(p, v_p);
    //test2(p, v_p);
    //test4(p);
    //test5(p);
    //test6(p);
    //test7(p);
    //wolverInterface0(p, v_p);
    wolverInterface1(p, v_p);
    //wolverInterface2(p, v_p);
    //wolverInterface3(p, v_p);
    return 0;
}*/

Prop* TwoPropfindInterpolant(vector<Prop*> v_p){
    std::string str,s;
    vector<string> vs;
    
    //cout << "give the position of your werePrincess" << endl;
    //cin >> s;

    piped_processt p(s, vs);
    str = CombineExpr2String(v_p);
    cout << str << endl;
    p.write(str);
    p.write("interpolate.\n");
    str = p.read_line();
    while (str != ".") {  // wait for the end of the response
      if(str.compare("VALID") == 0 && str.compare("INVALID") == 0){
          if(str.compare("INVALID") == 0){
        	  break;
          }
      }
      else{
          if(str.compare("true") != 0 && str.compare("false") != 0){
              PrincessFormulaParser pfp(str);
              return pfp.parse();
          }
      }
      str = p.read_line();
    }
}

Prop* InterpolantInterface(Prop *p1, Prop *p2, piped_processt &p_server){
    string s_princess, result_princess;
    vector<Prop*> v_princess;
    Prop *result_Prop=NULL;
    v_princess.push_back(p1);
    v_princess.push_back(p2);
    s_princess = CombineExpr2String(v_princess);
    p_server.write(s_princess);
    cout << "s_princess = " << s_princess << endl;
    p_server.write("interpolate.\n");
    result_princess = p_server.read_line();
    while (result_princess != ".") {  // wait for the end of the response
        cout << "result_princess = [" << result_princess << "] "<< endl;
        if(result_princess.compare("VALID") == 0 || result_princess.compare("INVALID") == 0){
            if(result_princess.compare("INVALID") == 0){
                result_princess = p_server.read_line();
                result_Prop = NULL;
                //break;
                }
            else{
                //continue;
            }
        }
        else{
            if(result_princess.compare("true") != 0 && result_princess.compare("false") != 0 && result_princess.compare("(true) ") != 0 && result_princess.compare("(false) ") != 0){
                PrincessFormulaParser pfp(result_princess);
                //p.push_back(pfp.parse());
                result_Prop = pfp.parse();
            }
        }
        result_princess = p_server.read_line();
    }
    return result_Prop;
}
